FDL - Step of Proof: fseg

Step of Proof: fseg_select

11,40

Inference at * 2 1 1 1 1
Iof proof for Lemma fseg select:

1. T : Type
2. l1 : T List
3. l2 : T List
4. ||l1||

||l2||
5.

. (i < ||l1||)

(l1[i] = l2[((||l2|| - ||l1||)+i)])

||l1|| = ||nth_tl(||l2|| - ||l1||;l2)||

by ((RWO "length_nth_tl" 0)

CollapseTHEN (Auto'))

Definitions nth_tl(n;as), P Q, P Q, P & Q, x:A B(x), , {x:A| B(x)} , , #$n, , A, False, P Q, Void, a < b, n+m, -n, {i...j}, ||as||, i j , x:A. B(x), x:AB(x), A B, type List, Type, s = t, t T, n - m

Lemmas iff wf, rev implies wf, length nth tl, nat wf, member wf, le wf, non neg length

Definitions	nth_tl(n;as), P Q, P Q, P & Q, x:A B(x), , {x:A\| B(x)} , , #$n, , A, False, P Q, Void, a < b, n+m, -n, {i...j}, \|\|as\|\|, i j , x:A. B(x), x:AB(x), A B, type List, Type, s = t, t T, n - m
Lemmas	iff wf, rev implies wf, length nth tl, nat wf, member wf, le wf, non neg length